es:ES, ff:FIFO, f2f+:F2F+-decls.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (sndr, rcvr:ff.C, y:E. [y: rcvr is_ack  sndr]  (z:E. f2f+-pred(z,y))) 

latex

Definitions	{T}, P  Q, [e: i p j], , x:A. B(x), A c B, x(s), f2f+-pred(e',e), t  T, P & Q, P  Q, x:A. B(x), [e: i p j], False, A, x  {FDLNOr12445}
Lemmas	not wf, es-causl wf, es-causle weakening, es-causl weakening, req-received-before-ack, decidable rcv-it, es-causle wf, rcv-it wf, max-of-eventset, event system wf, FIFO wf, F2F+-decls wf, fifoS wf, fifoR wf, f2f+Owes wf, f2f+Wait wf, f2f+Req wf, plus-ify wf, fifoC wf, es-E wf, f2f+Ack wf, snd-it wf, f2f+-property